Nuprl Lemma : wellfounded_wf 9,38

A:Type{i}, r:(AA{i}). WellFnd{i}(A;x,y.r(x,y))  {i'} 
latex


ProofTree


Definitionsx(s), P  Q, x(s1,s2), WellFnd{i}(A;x,y.R(x;y)), t  T, , x:AB(x)
Lemmasguard wf

origin